for clients C sends FIFO
forfrom j to i via (S[j,i],codes)
forreceives at i via (R[i],decodes)
== i:C.
== f:{e:E| R(i,e)} {e:E| j:C. (S(j,i,e))} 
== (e.j:C. (S(j,i,e))  f e.R(i,e)
== & (e:{e:E| R(i,e)} , j:{j:C| S(j,i,f(e))} .
== & (decodes(i,e,(state when e)) = codes(j,i,f(e),(state when f(e))))
== & (e, e':{e:E| R(i,e)} , j:C.
== & ((S(j,i,f(e)))  (S(j,i,f(e')))  f(e) c f(e')  e c e')) 

latex

---

clarification:

fifo(es;codes;decodes;C;S;R;T)
== i:C.
== f:{e:es-E(es)| R(i,e)} {e:es-E(es)| j:C. (S(j,i,e))} 
== (antecedent-surjection(es;e.R(i,e);e.j:C. (S(j,i,e));f)
== & (e:{e:es-E(es)| R(i,e)} , j:{j:C| S(j,i,f(e))} .
== & (decodes(i,e,es-state-when(es;e)) = codes(j,i,f(e),es-state-when(es;f(e)))  T)
== & (e:{e:es-E(es)| R(i,e)} , e':{e:es-E(es)| R(i,e)} , j:C.
== & ((S(j,i,f(e)))  (S(j,i,f(e')))  es-causle(es;f(e);f(e'))  es-causle(es;e;e'))) 

latex

Definitions	x:AB(x), P & Q, Q  f P, x.A(x), x:A. B(x), s = t, (state when e), {x:A| B(x)} , E, x:A. B(x), P  Q, f(a), e c e'
FDL editor aliases	fifo